ecl-machine2(i; ds; da; x; T; ks; a; upd)
== Rall(update-spec-vars(upd);
== Rall(z.R-state-var(i;
== Rall(z.R-state-var(fpf-join(id-deq; ds; fpf-single(x; T));
== Rall(z.R-state-var(da;
== Rall(z.R-state-var(z;
== Rall(z.R-state-var(fpf-ap(ds; id-deq; z);
== Rall(z.R-state-var(ks;
== Rall(z.R-state-var((k,s,v,z'. list_accum(z',nf.let n,f = nf
== Rall(z.R-state-var((k,s,v,z'. list_accum(in
== Rall(z.R-state-var((k,s,v,z'. list_accum(if a(n,k,s,v,s(x)) then f(s,v) else z' fi ;
== Rall(z.R-state-var((k,s,v,z'. list_accum(z';
== Rall(z.R-state-var((k,s,v,z'. list_accum(fpf-cap(upd;
== Rall(z.R-state-var((k,s,v,z'. list_accum(fpf-cap(product-deq(Knd; Id; Kind-deq; id-deq);
== Rall(z.R-state-var((k,s,v,z'. list_accum(fpf-cap(<k, z>;
== Rall(z.R-state-var((k,s,v,z'. list_accum(fpf-cap([]))))) 

latex

Definitions	Rall(L; x.R(x)), update-spec-vars(upd), R-state-var(i; ds; da; x; T; ks; tr), fpf-join(eq; f; g), fpf-single(x; v), fpf-ap(f; eq; x), x.A(x), list_accum(x,a.f(x;a); y; l), let x,y = A in B(x;y), if b then t else f fi , f(a), fpf-cap(f; eq; x; z), product-deq(A; B; a; b), Knd, Id, Kind-deq, id-deq, <a, b>, []
FDL editor aliases	ecl-machine2